/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#9=MATH55
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ¬¬TRULY INVARIANT ASSERTIONS

␈↓ α∧␈↓␈↓ αTThis␈α
is␈αa␈α
variant␈αof␈α
the␈αinvariant␈α
assertion␈α
method␈αfor␈α
proving␈αprograms␈α
correct.␈α The␈α
idea
␈↓ α∧␈↓is␈α⊂to␈α⊃use␈α⊂assertions␈α⊃that␈α⊂are␈α⊂true␈α⊃at␈α⊂all␈α⊃program␈α⊂points␈α⊂and␈α⊃whose␈α⊂truth␈α⊃is␈α⊂preserved␈α⊃by␈α⊂the
␈↓ α∧␈↓execution␈α∞of␈α∞all␈α∞statements.␈α∞ The␈α∂existence␈α∞of␈α∞such␈α∞␈↓↓truly␈α∞invariant␈α∞assertions␈↓␈α∂(abbreviated␈α∞TIA)
␈↓ α∧␈↓may␈αdepend␈α
on␈αthe␈α
presence␈αof␈α
additional␈α␈↓↓ghost␈α
variables␈↓␈αin␈α
the␈αprogram.␈α
 The␈αmain␈α
utility␈αof␈α
the
␈↓ α∧␈↓TIA␈α⊂method␈α∂is␈α⊂expected␈α⊂to␈α∂be␈α⊂for␈α∂proving␈α⊂correctness␈α⊂of␈α∂programs␈α⊂with␈α⊂concurrent␈α∂processes,
␈↓ α∧␈↓because it can help avoid considering n-tuplets of program points.

␈↓ α∧␈↓␈↓ αTWe␈α
shall␈α
proceed␈α
by␈α
discussing␈α
two␈α
examples.␈α
 The␈α
first␈α
is␈α
a␈α
program␈α
discussed␈α
by␈αSusan
␈↓ α∧␈↓Owicki at the WG2.2 meeting in Tampere, Finland, August 1976.  Owicki's program is


␈↓ α∧␈↓↓␈↓ ∧ts ← 0

␈↓ α∧␈↓↓␈↓ ∧t␈↓αcobegin␈↓↓



␈↓ α∧␈↓↓␈↓ αts ← s + f(x)␈↓ ¬ts ← s + g(x)



␈↓ α∧␈↓↓␈↓ ∧t␈↓αcoend␈↓




␈↓ α∧␈↓␈↓ αTThe␈α
object␈α
is␈α
to␈αprove␈α
that␈α
when␈α
the␈αprogram␈α
terminates,␈α
we␈α
have␈α␈↓↓s␈α
=␈α
f(x)␈α
+␈αg(x)␈↓,␈α
regardless
␈↓ α∧␈↓of␈αthe␈αorder␈αin␈αwhich␈αthe␈αparallel␈αoperations␈αare␈αcarried␈αout,␈αbut␈αwith␈αthe␈αobvious␈αcondition␈αthat
␈↓ α∧␈↓each␈α
assignment␈α
statement␈α
is␈αcarried␈α
out␈α
without␈α
interference.␈α
 In␈αorder␈α
to␈α
get␈α
suitable␈α
TIAs,␈αwe
␈↓ α∧␈↓add Boolean ghost variables ␈↓↓p␈↓ and ␈↓↓q,␈↓ so that the program becomes


␈↓ α∧␈↓↓␈↓ ∧ts ← 0
␈↓ α∧␈↓↓␈↓ ∧tp ← q ← ␈↓αfalse␈↓↓

␈↓ α∧␈↓↓␈↓ ∧t␈↓αcobegin␈↓↓



␈↓ α∧␈↓↓␈↓ αts ← s + f(x)␈↓ ¬ts ← s + g(x)
␈↓ α∧␈↓↓␈↓ αtp ← ␈↓αtrue␈↓↓␈↓ ¬tq ← ␈↓αfalse␈↓↓



␈↓ α∧␈↓↓␈↓ ∧t␈↓αcoend␈↓
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓␈↓ αTWe␈α
assume␈αthat␈α
each␈α
boxed␈αset␈α
of␈α
statements␈αis␈α
carried␈α
out␈αunitarily.␈α
 The␈α
␈↓↓truly␈αinvariant
␈↓ α∧␈↓↓assertion␈↓ is

␈↓ α∧␈↓␈↓ αT␈↓↓(¬p ∧ ¬q ∧ s=0) ∨ (p ∧ ¬q ∧ s=f(x)) ∨ (¬p ∧ q ∧ s=g(x)) ∨ (p ∧ q ∧ s=f(x)+g(x))␈↓,

␈↓ α∧␈↓taking␈αinto␈αaccount␈αeach␈αpair␈αof␈αprogram␈α
points.␈α However,␈αit␈αcan␈αalso␈αbe␈αwritten␈α
more␈αelegantly
␈↓ α∧␈↓as

␈↓ α∧␈↓␈↓ αT␈↓↓s = (␈↓αif ␈↓↓p ␈↓αthen ␈↓↓f(x)␈↓α else ␈↓↓0) + (␈↓αif ␈↓↓q ␈↓αthen ␈↓↓g(x) ␈↓α else ␈↓↓0)␈↓.

␈↓ α∧␈↓Either form of the assertion is true at all pairs of program points.

␈↓ α∧␈↓␈↓ αTWe give a second more elaborate example:

␈↓ α∧␈↓␈↓αbegin
␈↓ α∧␈↓α        integer ␈↓↓n, s; ␈↓αprocessor array ␈↓↓proc[1:500];

␈↓ α∧␈↓↓␈↓αboolean array ␈↓↓q[1:500], r[1:500];

␈↓ α∧␈↓↓        s ← 0; n ← 0;

␈↓ α∧␈↓↓␈↓αfor ␈↓↓i ← 1:500 ␈↓αdo begin ␈↓↓q[i] ← r[i] ← ␈↓αfalse end␈↓↓;

␈↓ α∧␈↓↓        ␈↓αfor␈↓↓ i ← 1:500␈↓α do start ␈↓↓proc[i];

␈↓ α∧␈↓↓        ␈↓αif␈↓↓ super(i) ␈↓αthen

␈↓ α∧␈↓α                begin

␈↓ α∧␈↓α                        for ␈↓↓j ← 1:500 ␈↓αdo if␈↓↓ j≠i ␈↓αthen kill␈↓↓ proc[j];

␈↓ α∧␈↓↓                        s ← 1000;  q[i] ← ␈↓αtrue␈↓↓;

␈↓ α∧␈↓↓                        ␈↓αgo to␈↓↓ done;

␈↓ α∧␈↓↓                ␈↓αend␈↓↓;

␈↓ α∧␈↓↓        ␈↓αif ␈↓↓good(i) ␈↓αthen ␈↓↓s ← s + 1;

␈↓ α∧␈↓↓        ␈↓αprotect begin

␈↓ α∧␈↓α                ␈↓↓n ← n + 1;

␈↓ α∧␈↓↓                ␈↓αif ␈↓↓n < 500 ␈↓αthen kill ␈↓↓proc[i]; r[i] ← ␈↓αtrue␈↓↓

␈↓ α∧␈↓↓        ␈↓αend

␈↓ α∧␈↓αend␈↓↓;

␈↓ α∧␈↓↓done:
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓␈↓ αTThe␈αidea␈αof␈αthis␈αprogram␈αis␈αthat␈αit␈αsets␈αup␈α500␈αprocesses␈αeach␈αof␈αwhich␈αtests␈αan␈α␈↓↓i␈↓␈αbetween␈α
1
␈↓ α∧␈↓and␈α500.␈α If␈αa␈αprocess␈αfinds␈αan␈α␈↓↓i␈↓␈αsatisfying␈α␈↓↓super(i),␈↓␈αit␈αsets␈α␈↓↓s␈↓␈αto␈α1000,␈αstops␈αall␈αthe␈αother␈αprocesses
␈↓ α∧␈↓and␈α
goes␈αto␈α
␈↓↓done.␈↓␈α
If␈α␈↓↓i␈↓␈α
statisfies␈α␈↓↓good(i),␈↓␈α
then␈α
it␈αadds␈α
1␈αto␈α
the␈α
count␈α␈↓↓s,␈↓␈α
and␈αcommits␈α
suicide␈α
if␈αit
␈↓ α∧␈↓isn't␈αthe␈αlast␈αprocessor␈αto␈αfinish.␈α The␈αBoolean␈αvariables␈α␈↓↓q[1:500]␈↓␈αand␈α␈↓↓r[1:500]␈↓␈αare␈αghost␈αvariables
␈↓ α∧␈↓used␈α
only␈α
in␈α
writing␈α
the␈α
TIA.␈α
 I␈αdon't␈α
especially␈α
advocate␈α
the␈α
notation␈α
used␈α
for␈αparallel␈α
processing.
␈↓ α∧␈↓It␈α∞is␈α∞ad␈α∂hoc␈α∞for␈α∞the␈α∂example.␈α∞ It␈α∞may␈α∂need␈α∞to␈α∞be␈α∂said␈α∞that␈α∞each␈α∂process␈α∞starts␈α∞at␈α∂the␈α∞statement
␈↓ α∧␈↓following the statement that creates them.

␈↓ α∧␈↓␈↓ αTThe TIA is


␈↓ α∧␈↓␈↓ αT␈↓↓s = ␈↓αif ␈↓↓(∃k.q[k] ∧ super(k)) ␈↓αthen ␈↓↓1000 ␈↓αelse ␈↓	$␈↓↓(␈↓αif ␈↓↓r[k] ∧ good(k) ␈↓αthen ␈↓↓1 ␈↓αelse ␈↓↓0)␈↓.


␈↓ α∧␈↓It␈α
is␈α
easily␈αverified␈α
that␈α
this␈αassertion␈α
is␈α
true␈αat␈α
all␈α
n-tuplets␈αof␈α
program␈α
points,␈α
making␈αsuitable
␈↓ α∧␈↓assumptions about the completion of statements without interference.

␈↓ α∧␈↓␈↓ αTPerhaps the idea can also be applied to intermittent assertions.


␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, CA 94305